{-# LANGUAGE TypeFamilies, Rank2Types, TypeOperators, MultiParamTypeClasses #-}

{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances,
  ConstraintKinds, ScopedTypeVariables #-}

module Convert (Cnv, Convert(..), convertDCs) where

import TypeBasics
import Yoko
import RPV
import Each
import Map
import OnRs



-- TODO could generalize FindDCs over the "\x y -> tag x `isPrefixOf` tag y"
-- relation



-- there are actually ~15 lines, once you drop the nice formatting
type family FindDCs s sum
type instance FindDCs s (N dc) =
  If (IsPrefixOf s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+ b) = DistMaybePlus (FindDCs s a) (FindDCs s b)





type family Cnv cnv a
class Convert cnv a where convert :: cnv -> a -> Cnv cnv a

data CnvRPV cnv a = CnvRPV cnv
type instance Con  (CnvRPV cnv) a = Convert cnv a
type instance Inst (CnvRPV cnv) a = a -> Cnv cnv a
instance RPV (CnvRPV cnv) where instantiate (CnvRPV cnv) = convert cnv





class (Generic dc, a ~ Range dc, Map (OnRsRPV (CnvRPV cnv)) (Rep dc)
      ) => ConvertDC cnv a dc where
  convertDC :: cnv -> Proxy a -> dc -> Cnv cnv a
instance (Generic dc, a ~ Range dc, Map (OnRsRPV (CnvRPV cnv)) (Rep dc),
          -- NB must match exactly one constructor, thus no ambiguity
          Just (N dc') ~ FindDCs (Tag dc) (DCs (Cnv cnv a)),
          Rep dc' ~ Mapped (OnRsRPV (CnvRPV cnv)) (Rep dc),
          DC dc', Cnv cnv a ~ Range dc'
         ) => ConvertDC cnv a dc where
  convertDC cnv _ =
    rejoin . (id :: dc' -> dc') . obj . mapRPV (onRsRPV (CnvRPV cnv)) . rep



convertDCs :: forall cnv sum a.
  Each (ConvertDC cnv a) sum => cnv -> DCsOf a sum -> Cnv cnv a
convertDCs cnv = each (Proxy :: Proxy (ConvertDC cnv a)) $
  convertDC cnv (Proxy :: Proxy a)
